COMMENT ⊗   VALID 00009 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require"lispub.pub[206,lsp]"source
C00003 00003	.sEC		 PROVING LISP PROGRAMS CORRECT
C00005 00004	.ss First order logic with conditional forms and lambda-expressions.
C00017 00005	.ss Conditional forms.
C00023 00006	.ss Lambda-expressions.
C00025 00007	.ss Algebraic axioms for S-expressions and lists.
C00029 00008	.ss Axiom schemas of induction.
C00031 00009	.ss Proofs by structural induction.
C00034 ENDMK
C⊗;
.require"lispub.pub[206,lsp]"source
.turn on "→∂{"
.sEC		 PROVING LISP PROGRAMS CORRECT

	In this chapter we will introduce techniques for proving
LISP programs correct.
The techniques will mainly be limited to what we may call %3clean%1
LISP programs.  In particular, there must be no side effects,
because our methods depend on the ability to replace subexpressions
by equal expressions.

	The  necessary basic facts can be divided into several categories:
first order logic including conditional forms and first order
lambda-expressions,
algebraic facts about lists and S-expressions,
facts about the inductive structure of lists and
S-expressions, and general facts about functions defined by
recursion.  Ideally, we would use a general theory of recursive
definition to prove theorems about LISP functions.  However,
the general theory is not well enough developed, so we have had
to introduce some methods limited to LISP functions defined by
particular kinds of recursion schemes.

.ss First order logic with conditional forms and lambda-expressions.

	The logic we shall use is called first order logic with equality,
but we will extend it by allowing conditional forms to be terms and
lambda-expressions to be function expressions.  From the mathematical
point of view, these extensions are inessential, because, as we shall see,
every sentence that includes conditional forms or first order lambdas can
readily be transformed into an equivalent sentence without them.  However,
the extensions are practically important, because they permit us to use
certain recursive definitions directly as formulas of the logic.
Unfortunately, we will not be able to treat all recursive definitions
in this system, but only those which we can be sure are defined for
all values of the arguments.  Moreover, we will be unable to prove
definedness within the system, so we will be restricted to classes
of recursive definitions which we can prove always defined by
an argument outside the system.  Fortunately, many interesting
LISP functions meet these restrictions including all the important
functions so far used except for %3eval%1 and its variants.

	Formulas of the logic are built from constants, variables
predicate symbols, and function symbols using function application,
conditional forms, boolean forms, lambda expressions, and quantifiers.

%4Constants%1: We will use S-expresssions as constants standing for
themselves and also lower case letters from the first part
of the alphabet to represent constants in other domains than
S-expressions.

%4Variables%1: We will use the letters %3u%1 thru %3z%1 with or
without subscripts as variables.

%4Function symbols%1: The letters %3f%1, %3g%1 and %3h%1 with or
without subscripts are used as function symbols.
The LISP function symbols %4a%1, %4d%1 and . (as an infix) are also
used as function symbols.
We suppose that each function symbol takes the same definite number of
arguments every time it is used.

%4Predicate symbols%1: The letters %3p%1, %3q%1 and %3r%1 with or
without subscripts are used as predicate symbols.  We will
also use the LISP predicate symbol %4at%1 as a constant predicate
symbol.  The equality symbol = is also used as an infix.
We suppose that each predicate symbol takes the same definite
number of arguments each time it is used.

	Next we define terms, sentences, function expressions
and predicate expressions inductively.  A term is
an expression whose value will be an object like an S-expression
or a number while a sentence has value %5T%1 or %5F%1.
Terms are used in making sentences, and sentences occur in
terms so that the definitions are %3mutually recursive%1 where
this use of the word %3recursive%1 should be distinguished from
its use in recursive definitions of functions.
Function expressions are also involved in the mutual recursion.

%4Terms%1: Constants are terms, and variables are terms.  If
%3f%1 is a function expression taking %3n%1 arguments, and %3t%61%3,#...#,t%6n%3%1
are terms, then %3f[t%61%3,#...#,t%6n%3]%1 is a term.  If %3p%1 is
a sentence and %3t%61%3%1 and %3t%62%1 are terms, then
%4if%3#p#%4then%3#t%61%3#%4else%3#t%62%1%1 is a term.  We soften the
notation by allowing infix symbols where this is customary.

%4Sentences%1:
If %3p%1 is a predicate expression taking %3n%1 arguments and
%3t%61%3,#...#,t%6n%3%1 are terms, then %3p[t%61%3,#...#,t%6n%3]%1 is
a sentence.  Equality is also used as an infixed predicate
symbol to form sentences, i.e. %3t%61%3#=#t%62%1%1 is a sentence.
If %3p%1 is a sentence, then %3¬p%1 is also a sentence.  If
%3p%1 and %3q%1 are sentences, then %3p∧q%1, %3p∨q%1, %3p⊃q%1,
and %3p≡q%1 are sentences.  If %3p%1, %3q%1 and %3r%1 are
sentences, then %4if%3#p#%4then%3#q#%4else%3#r%1 is a sentence.
If %3x%61%3,#...,#x%6n%3%1 are variables, and %3p%1 is a term, then
%3∀x%61%3#...#x%6n%3:t%1 and %3∀x%61%3#...#x%6n%3:t%1 are sentences.

%4Function expressions%1: A function symbol is a function expression.
If %3x%61%3,#...#,x%6n%3%1 are variables and %3t%1 is a term, then
%3[λx%61%3,#...#,x%6n%3:t]%1 is a function expression.

%4Predicate expressions%1: A predicate symbol is a predicate expression.
If %3x%61%3,#...#,x%6n%3%1 are variables and %3p%1 is a sentence, then
%3[λx%61%3,#...#,x%6n%3:p]%1 is a predicate expression.

	An occurrence of a variable %3x%1 is called bound if
it is in an expression of one of the forms %3[λx%61%3#...#x%6n%3:t]%1,
%3[λx%61%3#...#x%6n%3:p]%1, %3[∀x%61%3#...#x%6n%3:p]%1 or %3[∃x%61%3#...#x%6n%3:p]%1
where %3x%1 is one
of the numbered %3x%1's.  If not bound an occurrence is called free.

	The %3semantics%1 of first order logic consists of the rules
that enable us to determine when a sentence is true and when it
is false.  However, the truth or falsity of a sentence is relative
to the interpretation assigned to the constants, the function and predicate
symbols and the free variables of the formula.  We proceed as follows:

	We begin by choosing a domain.  In most cases we shall consider
the domain will include the S-expressions and any S-expression constants
appearing in the formula stand for themselves.  We will allow for the
possibility that other objects than S-expressions exist, and some constants
may designate them.  Each function or predicate symbol is assigned a
function or predicate on the domain.  We will normally assign to the
basic LISP function and predicate symbols the corresponding basic LISP
functions and predicates.  Each variable appearing free in a sentence is
also assigned an elemet of the domain.  All these assignments constitute
an interpretation, and the truth of a sentence is relative to the
interpretation.

	The truth of a sentence is determined from the values of its
constituents by evaluating successively larger subexpressions.  The
rules for handling functions and predicates, conditional expressions,
equality, and Boolean expressions are exactly the same as those we
have used in the previous chapters.  We need only explain quantifiers:

	%3∀x%61%3#...#x%6n%3:e%1 is assigned true if and only if %3e%1 is assigned
true for all assignments of elements of the domain to the %3x%1's.  If
%3e%1 has free variables that are not among the %3x%1's, then the
truth of the sentence depends on the values assigned to these remaining
free variables.  %3∃x%61%3#...#x%6n%3:e%1 is assigned true if and only if %3e%1
is assigned true for %3some%1 assignment of values in the domain to
the %3x%1's.  Free variables are handled just as before.

	%3λx%61%3#...#x%6n%3:u%1 is assigned a function or predicate according
to whether %3u%1 is a term or a sentence.  The value of
%3[λx%61%3#...#x%6n%3:u][t%61%3,...,t%6n%3] is obtained by evaluating the 
%3t%1's and using these values as values of the %3x%1's in the
evaluation of %3u%1.  If %3u%1 has free variables in addition to the %3x%1's,
the function assigned will depend on them too.

	Those who are familiar with the lambda calculus should note
that λ is being used here in a very limited way.  Namely, the variables
in a lambda-expression take only elements of the domain as values,
whereas the essence of the lambda calculus is that they take arbitrary
functions as values.  We may call these restricted lambda expressions
%3first order lambdas%1.
.ss Conditional forms.

	All the properties we shall use of conditional forms follow
from the relation

	%3[p ⊃ [%4if%3 p %4then %3a %4else%3 b] = a] ∧ [¬p ⊃ [%4if%3 p %4then%3 a
%4else%3b] = b]%1.

(If we weren't adhering to the requireement that all terms be defined for
all values of the variables, the situation would be more complicated).

	It is, however, worthwhile to list separately some properties
of conditional forms.

	First we have the obvious

	%4if%5#T#%4then%3#a#%4else%3#b%3 = a%1

and

	%4if%5#F#%4then%3#a#%4else%3#b%3 = b%1.

	Next we have a %3distributive law%1 for functions applied
to conditional forms, namely

	%3f[%4if%3 p %4then%3 a %4else%3 b] = %4if%3 p %4then%3 f[a] %4else%3 f[b]%1.

This applies to predicates as well as functions and can also be used
when one of the arguments of a function of several arguments is a
conditional form.  It also applies when one of the terms of
a conditional form is itself a conditional form.

Thus

	%4if%3 [%4if%3 p %4then%3 q %4else%3 r] %4then%3 a %4else%3 b =
%4if%3 p %4then%3 [%4if%3 q %4then%3 a %4else%3 b] %4else%3 [%4if%3 r
%4then%3 a %4else%3 b]%1

and

	%4if%3 p %4then%3 [%4if%3 q %4then%3 a %4else%3 b] %4else%3 c =
%4if%3 q %4then%3 [%4if%3 p %4then%3 a %4else%3 c] %4else%3 [%4if%3 p
%4then%3 b %4else%3 c]%1.

	When the expressions following %4then%1 and %4else%1 are
sentences, then the conditional form can be replaced by a sentence
according to

	%3[%4if%3 p %4then%3 q %4else%3 r] ≡ [p ∧ q] ∨ [¬p ∧ r]%1.

These two rules permit eliminating conditional forms from sentences
by first using distributivity to move the conditionals
to the outside of any functions and then replacing the conditional
form by a Boolean expression.

	Note that the elimination of conditional forms may increase
the size of a sentence, because %3p%1 occurs twice in the right
hand side of the above equivalence.  In the most unfavorable case,
%3p%1 is dominates the size of the expression so that writing it
twice almost doubles the size of the expression.

	Suppose that %3a%1 and %3b%1 in
%4if%3#p#%4then%3#a#%4else%3#b%1
are expressions that may contain the sentence %3p%1.  Occurrences
of %3p%1 in %3a%1 can be replaced by %5T%1, and occurrences of %3p%1
in %3b%1 can be replaced by %5F%1.  This follows from the fact that
%3a%1 is only evaluated if %3p%1 is true and %3b%1 is evaluated only
if %3p%1 is false.

	This leads to a strengthened form of the law of replacement
of equals by equals.  The ordinary form of the law says that if
we have %3e#=#e'%1, then we can replace any occurrence of %3e%1
in an expression by an occurrence of %3e'%1.  However, if we want
to replace %3e%1 by %3e'%1 within %3a%1 within
%4if%3#p#%4then%3#a#%4else%3#b%1,
then we need only prove %3p#⊃#e#=e'%1, and to make the replacement
within %3b%1 we need only prove %3¬p#⊃#e#=#e'%1.

	Additional facts about conditional forms are given in (McCarthy 1963a)
including a discussion of canonical forms that parallels the canonical
forms of Boolean forms.  Any question of equivalence of conditional
forms is decidable by truth tables analogously to the decidability of
Boolean forms.
.ss Lambda-expressions.

	The only additional rule required for handlying lambda-expressions
in first order logic is called %3lambda-conversion%1, essentially

	%3[λx:e][a] =%1 <the result of substituting %3e%1 for %3x%1 in %3a%1>.

As examples of this rule, we have

	%3[λx:%4a%3 x . y][u . v] = [%4a%3[u . v]] . y%1.

However, a complication requires modifying the rule.  Namely,
we can't substitute for a variable and expression that has a free variable
into a context in which that free variable is bound.  Thus it would be
wrong to substitute %3x#+#y%1 for %3x%1 in %3∀y:[x#+#y#=#z]%1 or into
the term %3[λy:x#+#y][u#+#v]%1.  Before doing the substitution, the
variable %3y%1 would have to be replaced in all its bound occurrences by
a fresh variable.

	Lambda-expressions can always be eliminated from sentences and
terms by lambda-conversion, but the expression may increase greatly
in length if a lengthy term replaces a variable that occurs more than
once in %3e%1.  It is easy to make an expression of length %3n%1 whose
length is increased to 2%7n%1 by converting its %3n%1 nested lambda-expressions.

.ss Algebraic axioms for S-expressions and lists.

	The algebraic facts about S-expressions are expressed
by the following sentences of first order logic:

	%3∀x.(issexp x ⊃ %4at%3 x ∨ (issexp %4a%3 x ∧ issexp %4d%3 x
∧ x = (%4a%3 x . %4d%3 x)))%1

and

	%3∀x y.(issexp x ∧ issexp y ⊃ issexp(x.y) ∧ ¬%4at%3(x.y)
∧ x = %4a%3(x.y) ∧ y = %4d%3(x.y))%1.

Here %3issexp e%1 asserts that the object %3e%1 is an S-expression
so that the sentences used in proving a particular program correct
can involve other kinds of entities as well.
If we can assume that all objects are S-expressions or can declare certain
variables as ranging only over S-expressions, we can simplify the axioms
to

	%3∀x.[%4at%3 x ∨ x = [%4a%3 x . %4d%3 x]]%1

and

	%3∀x y.[¬%4at%3[x.y] ∧ x = %4a%3[x.y] ∧ y = %4d%3[x.y]]%1.


	The algebraic facts about lists are expressed by the following
sentences of first order logic:

	%3∀x. islist x ⊃ x = %5NIL%3 ∨ islist %4d %3x%1,

	%3∀x y. islist y ⊃ islist[x . y]%1,

	%3∀x y. islist y ⊃ %4a%3[x . y] = x ∧ %4d%3[x.y] = y%1.

We can rarely assume that everything is a list, because the
lists usually contain atoms which are not themselves lists.

	These axioms are analogous to the algebraic part of Peano's
axioms for the non-negative integers.  The analogy can be made clear
if we write Peano's axioms using %3n'%1 for the successor of %3n%1
and %3n%7-%1 for the predecessor of %3n%1.  Peano's algebraic axioms
then become

	%3∀n: n' ≠ 0%1,

	%3∀n: (n')%7-%3 = n%1,

and

	%3∀n: n ≠ 0 ⊃ (n%7-%3)' = n%1.

Integers specialize  lists if we identify 0 with %5NIL%1 and assume that
there is only one object (say 1) that can serve as a list element.
Then %3n'#=#cons[1,n]%1, and %3n%7-%3#=#%4d%3 n%1.

	Clearly S-expressions and lists satisfy the axioms given for them,
but unfortunately these algebraic axioms are insufficient to
characterize them.  For example, consider a domain of one element
%2a%1 satisfying

	%4a%3 a = %4d%3 a = a . a = a%1.

It satisfies the algebraic axioms for S-expressions.  We can exclude
it by an axiom %3∀x.(%4a%3 x ≠ x)%1, but this won't exclude other
circular list structures that eventually return to the same element
by some %4a-d%1 chain.  Actually we want to exclude all infinite
chains, because most LISP programs won't terminate unless every
%4a-d%1 chain eventually terminates in an atom.  This cannot be
done by any finite set of axioms.

.ss Axiom schemas of induction.

	
	In order to exclude infinite list structures we need axioms
of induction analogous to Peano's induction axiom.  Peano's axiom
is ordinarily written

	%3P(0) ∧ ∀n:(P(n) ⊃ P(n')) ⊃ ∀n:P(n)%1.

Here %3P(n)%1 is an arbitrary predicate of integers, and we get particular
instances of the axiom by substituting particular predicates.

Peano's induction schema can also be written 

	%3∀n:(n = 0 ∨ P(n%7-%3) ⊃ P(n)) ⊃ ∀n:P(n)%1,

and the equivalence of the two forms is easily proved.

	The S-expression analog is

	%3∀x:[issexp x ⊃ [%4at%3 x ∨ P[%4a%3 x] ∧ P[%4d%3 x] ⊃ P[x]]] ⊃
∀x:[issexp x ⊃ P[x]]%1,

or, assuming everything is an S-expression

	%3∀x:[%4at%3 x ∨ P[%4a%3 x] ∧ P[%4d%3 x] ⊃ P[x]] ⊃ ∀x:P[x]%1.

	The corresponding axiom schema for lists is

	%3∀u:[islist u ⊃ [%4n%3 u ∨ P[%4d%3 u] ⊃ P[u]]] ⊃ ∀u:[islist u
⊃ P[u]]%1.

	These schemas are called principles of %3structural induction%1,
since the induction is on the structure of the entities involved.
.ss Proofs by structural induction.

	Recall that the operation of appending two lists is defined by

!!si2:	%3u * v ← %4if n%3 u %4then%3 v %4else a%3 u . [%4d%3 u * v]%1.

Because %3u*v%1 is defined for all %3u%1 and %3v%1, i.e. the computation
described above terminates for all %3u%1 and %3v%1, we can replace ({[5] si2})
by the sentence

!!si1:	%3∀u v:[islist u ∧ islist v ⊃
[%3u * v = %4if n%3 u %4then%3 v %4else a%3 u . [%4d%3 u * v]]]%1.

Now suppose we would like to prove %3∀v:[%5NIL%3 * v = v]%1.  This is
quite trivial; we need only substitute %5NIL%1 for %3x%1 in ({[5] si1}),
getting

→%5NIL%3 * v ∂(15)#= %4if n %5NIL %4then%3 v %4else a %5NIL%3 . [%4d %5NIL%3 * v]

∂(15)#= v%1.

Next consider proving %3∀u:[u * %5NIL%3 = u]%1.  This cannot be done by
simple substitution, but it can be done as follows:  First substitute
%3λu:[u * %5NIL%3 = u]%1 for %3P%1 in the induction schema

	%3∀u:[islist u ⊃ [%4n%3 u ∨ P[%4d%3 u] ⊃ P[u]]] ⊃ ∀u:[islist u
⊃ P[u]]%1,

getting

	%3∀u:[islist u ⊃ [%4n%3 u ∨ %3λu:[u * %5NIL%3 = u][%4d%3 u]
⊃ %3λu:[u * %5NIL%3 = u][u]]] ⊃ ∀u:[islist u
⊃ %3λu:[u * %5NIL%3 = u][u]]%1.

Carrying out the indicated lambda conversions makes this

!!si3:	%3∀u:[islist u ⊃ [qn u ∨ qd u * qNIL = qd u]
⊃ u * qNIL = u] ⊃ ∀u:[islist u ⊃ u * qNIL = u]%1.